Univalence Axiom (UA)
同一性に関する公理の一つ
公理なので証明はされない？
Univalenceのいい訳し方は未だによくわからない
下記ページで自分の見解をメモしておく
→Univalence Axiomの訳
Univalence Axiomはホモトピー型理論で使われている
ホモトピー同値である型同士は同じ型であるとみなしてよいことを保証する公理([関山2024])
Univalent Foundationsの重要な公理の一つ？
同一視型(identity type)
Univalence Axiom関連の動画
CIRM - Videos & books Library - Search by event
CIRM - Videos & books Library - Dans tout Kentika
Univalence Axiom(UA)に関するいろいろな実装
HoTTの実装
Coq-HoTT
Cubical Type Theoryの実装
Cubical Agda
一価性公理 -- ホモトピー型理論
【1211.2851】 The Simplicial Model of Univalent Foundations (after Voevodsky)
Structuralism, Invariance, and Univalence
定義
型$ A, B
$ (A = B) ≃ (A ≃ B)
$ \text{equiv-eq} : (A = B) \to (A ≃ B)
確認用
Q. Univalence Axiom
Q. 何がうれしいか
関連
Univalence
同値関係
宇宙型
型宇宙
依存型理論
可縮性
参考
univalence axiom in nLab
[関山2024] Physics Lab. 2024『計算物理班 新たな数学としてのホモトピー型理論』
「同じ」を考える -- Univalence Axiom 入門 | MaruLabo
https://www.youtube.com/watch?v=LUcTKi-nGUQ
#Homotopy_Type_Theory(HoTT)